(declare-fun a () RoundingMode)
(declare-fun b () RoundingMode)
(declare-fun c () RoundingMode)
(declare-fun e () RoundingMode)
(declare-fun d () (_ FloatingPoint 8 24))
(declare-fun f () (_ FloatingPoint 8 24))
(declare-fun o () (_ FloatingPoint 8 24))
(declare-fun g () (_ FloatingPoint 8 24))
(declare-fun h () (_ FloatingPoint 8 24))
(declare-fun aa () (_ FloatingPoint 8 24))
(declare-fun i () (_ FloatingPoint 8 24))
(declare-fun j () (_ FloatingPoint 8 24))
(declare-fun bb () (_ FloatingPoint 8 24))
(declare-fun n () (_ FloatingPoint 8 24))
(declare-fun p () (_ FloatingPoint 8 24))
(declare-fun q () (_ FloatingPoint 8 24))
(declare-fun k () (_ FloatingPoint 8 24))
(declare-fun cc () (_ FloatingPoint 8 24))
(declare-fun l () (_ FloatingPoint 8 24))
(assert (distinct c b))
(assert (distinct c a))
(assert (distinct e roundNearestTiesToEven))
(assert (not (= (ite (let ((m ((_ to_fp 8 24) e (/ 7.0 5.0)))) (and (fp.lt f m) (fp.geq f (fp.neg m)))) (_ bv1 32) (_ bv0 32)) (_ bv0 32))))
(assert (= f d f))
(assert (= g o))
(assert (= aa h))
(assert (distinct i f))
(assert (= bb j))
(assert (distinct n (fp.sub e f (fp.add e aa bb))))
(assert (distinct p n))
(assert (= q p))
(assert (distinct cc k))
(assert (not (fp.eq ((_ to_fp 11 53) e l) ((_ to_fp 11 53) e (/ 1.0 10.0)))))
(check-sat)
